T:(IdType), tab:secret-table(T), x:Atom1.
isl(st-lookup(tab;x))
 (n:||tab|| .
 (nptr(tab)
 (& st-atom(tab;n) = x
 (& outl(st-lookup(tab;x)) = <key(tab;n),data(tab;n)>  (+Atom1)data(T)) 

latex

Definitions	x:A. B(x), P  Q, st-lookup(tab;x), ||tab|| , ptr(tab), st-atom(tab;n), let x,y,z = a in t(x;y;z), 1of(t), 2of(t), t  T, {i..j}, p  q, true, P  Q, Prop, P & Q, P  Q, if b t else f fi, false, T, True, x. t(x), i  j < k, x:A. B(x), b, secret-table(T), , , Unit, x(s),
Lemmas	assert wf, isl wf, nat wf, data wf, unit wf, st-lookup wf, secret-table wf, Id wf, mu wf, bool wf, iff transitivity, le wf, eqtt to assert, assert of le int, bor wf, btrue wf, lt int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int, eq atom wf1, pi1 wf, le int wf, bnot of lt int